Issue392.agda:29,11-13
Identifier f2 is declared irrelevant, so it cannot be used here
when checking that the expression f2 has type R1
